\begin{tabbing}
1. $T$ : Type
\\[0ex]2. $n$ : $\mathbb{Z}$
\\[0ex]3. 0 $<$ $n$
\\[0ex]4. \=$\forall$$m$:$\mathbb{N}$, $b$:$T$, $c$:(\{0..(($n$ {-} 1)+$m$)$^{-}$\}$\rightarrow$$T$$\rightarrow$$T$).\+
\\[0ex]primrec(($n$ {-} 1)+$m$;$b$;$c$) = primrec($n$ {-} 1;primrec($m$;$b$;$c$);$\lambda$$i$,$t$. $c$($i$+$m$,$t$))
\-\\[0ex]5. $m$ : $\mathbb{N}$
\\[0ex]6. $b$ : $T$
\\[0ex]7. $c$ : \{0..($n$+$m$)$^{-}$\}$\rightarrow$$T$$\rightarrow$$T$
\\[0ex]8. ${\it b'}$ : $T$
\\[0ex]9. primrec($m$;$b$;$c$) = ${\it b'}$
\\[0ex]10. primrec(($n$ {-} 1)+$m$;$b$;$c$) = primrec($n$ {-} 1;${\it b'}$;$\lambda$$i$,$t$. $c$($i$+$m$,$t$))
\\[0ex]11. $\neg$($n$+$m$ = 0)
\\[0ex]12. $\neg$($n$ = 0)
\\[0ex]$\vdash$  $c$((($n$+$m$) {-} 1),primrec(($n$+$m$) {-} 1;$b$;$c$)) = $c$(($n$ {-} 1)+$m$,primrec($n$ {-} 1;${\it b'}$;$\lambda$$i$,$t$. $c$($i$+$m$,$t$)))
\end{tabbing}